Struct isotope::prelude::Refl [−][src]
pub struct Refl { /* fields omitted */ }
Expand description
The reflexivity axiom: asserts that the left hand side and right hand side are judgementally equal, and therefore propositionally equal
Implementations
Create a new, unchecked instance of the reflexivity axiom with a given annotation
Compute the most basic identity type for a given instance of the reflexivity axiom
Create a new, unchecked instance of the reflexivity axiom, inferring the most basic possible annotation
Compute the code of a reflexivity instance with a given type annotation
Compute the filter of a reflexivity instance with a given type annotation
Compute the flags of a reflexivity instance with a given type annotation
Compute whether a dependent function type locally type-checks given an annotation
Compute whether a dependent function type locally type-checks given an identity type
Get the left and right hand side of this path if equivalent
Get the left and side of this path if different from the right hand side
If both sides of this equality are universes, return one.
Return None
if neither side is a universe, or if both sides are different universes (implying this instance is invalid!)
Attempt to transport the right side of this path in a given typing context.
Get this path transported right in a given typing context
pub fn coerce_right(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]
pub fn coerce_right(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]Get this instance of reflexivity as a coerced annotation
Convert this annotation into it’s equal sides, or error if unequal
Trait Implementations
Cons this term within a given context. Return None
if already consed.
Convert this term to it’s own consed type
Whether this term depends on a variable with a given index: if equiv is true, also consider larger variables in the same equivalence class
Get whether a term depends on a variable base <= variable <= ix
Read more
Get the variable filter of this term
type Substituted = Refl
type Substituted = Refl
The type this substitutes to
Substitute this value recursively
Convert this object’s consed form to it’s substituted form
Shift this term’s variables with index >= base
in a given context
Shift this term’s variables with index >= base
in a given context
Locally typecheck a term: note this is context-independent, without caching
Globally typecheck a term, i.e. typecheck all subterms, without caching
Typecheck this term’s annotation, without caching
Load this term’s current flags
Set this term’s flags. May cause errors if done incorrectly!
Locally typecheck a term: note this is context-independent.
Globally typecheck a term, i.e. typecheck all subterms and their variables
Variable typecheck a term, i.e. typecheck all subterms and their variables.
Typecheck this term’s annotation
Globally typecheck a term and it’s annotation, i.e. typecheck all subterms, annotation subterms, and their variables
Typecheck a term in a given context
Typecheck this term along with it’s variables
Whether this term might be type-checked
type ValueConsed = Refl
type ValueConsed = Refl
The type of value this is consed to
type ValueSubstituted = Refl
type ValueSubstituted = Refl
The type of value this is substituted to
Convert this term to a Term
, without any consing
Get the type annotation of this term
Get whether this term is a type
Get whether this term is a universe
Get whether this term is a function
Get whether this term is a dependent function type
Coerce this term to another type, with type-checking
fn annotate_unchecked(
&self,
_annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Refl>, Error>
[src]
fn annotate_unchecked(
&self,
_annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<Refl>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in a given context
Get the hash-code of this term if it was untyped Read more
Compare this term to another within a given context
Get the index of this term in a program graph. Return None
if this term is unindexed
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in general
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]Cast this type into another in a given typing context
Substitute this term’s variables recursively given a context
Substitute this term’s variables given a context
Shift this term’s variables with index >= base
up by n
in a given context
Shift this term’s variables with index >= base
up by n
in a given context
Compare this term to a term ID, within a given context
Cons this term within a given context. Return None
if already consed.
Convert this term to a TermId
within a given context
Get the type of this term, if any
Get the type of this term, if any
Apply this value, as a function, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Apply this value, as a dependent function type, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Convert this term to a TermId
, without any consing
Clone this term to a TermId
, without any consing
Clone this term to a TermId
within a given context
Clone this term to a Term
without any consing
Shallow cons a term directly into a context
Shallow cons a term directly into a context, cloning if necessary
Convert this term to a normal form
Convert this term a normal form
Convert this term to a normal form, or reduce it up to n
steps
Convert this term a normal form, or reduce it up to n
steps
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to a normal form, or reduce it up to n
steps
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]Convert this term a normal form, or reduce it up to n
steps
Auto Trait Implementations
impl !RefUnwindSafe for Refl
impl !UnwindSafe for Refl
Blanket Implementations
Mutably borrows from an owned value. Read more
Borrow an optional value of type T
Compare self to key
and return true
if they are equal.